structure Codegen4Ir (*: CODEGEN *)=
struct
  structure A = Assem
  structure Ast = Ir
  structure Asst = Assert
  structure F = Frame4Ir
  structure T = Temp
  structure E = Env4Ir
  structure Err = ErrorMsg
  structure Tr = Transp
  structure Ts = ToString
  structure P = Proof2
  structure PG = Prfgen2
  structure LCoq = LCoqize2
  structure B = Build
(*

  fun buildSEnv id fieldlist senv = 
      let val sframe = F.newSFrame(id)
          val flist = ref [];
          fun enterfield (id, mytype) = 
              let val types = E.cvtType(mytype)
                  val fsize = E.calTypeSize types senv
                  val offset = F.allocFields sframe fsize
              in  flist := E.enter id (offset, types) (!flist)
              end
          val _ = List.app enterfield fieldlist
          val size = F.getFields(sframe)
      in  E.enterS id size (!flist) senv
      end
      
  fun buildGEnv gvlist env = 
      let val newenv = ref env
          fun enterenv (id, mytype) =
              let val types = E.cvtType(mytype)
              in  newenv := E.enter id (false, ~1, types) (!newenv)
              end
          val _ = List.app enterenv gvlist
      in  !newenv
      end
  fun buildFEnv (id, mytype) env =
      let val types = E.cvtType(mytype)
      in  E.enter id (false, ~2, types) env
      end

  fun buildEnv vdeclist env senv frame alloc = 
      let val newenv = ref env
          fun enterenv (id, mytype) = 
              let val types = E.cvtType(mytype)
                  val size = E.calTypeSize types senv
                  val offset = alloc frame size
              in newenv := E.enter id (true, offset, types) (!newenv)
              end
          val _ = List.app enterenv vdeclist
      in  !newenv
      end
*)      
(* action: when given frame,emit function of a function, creat prolog for it
 * Note: the size of locals of this function doesn't equal to getLocals only,
 *       but must subtract the size of callee-saved register 
 *)
  fun prolog frame pre env senv emit emitSpec on= 
      let val fid = F.getFname frame
          val loc = (F.getLocals frame) - (F.getRegSize ())
          val funstart = T.newLabel()
          val precond1 = if on 
                         then Tr.transProp pre false env senv
                         else (fn (s:Asst.state)=>Asst.True)
          val precond2 = if on
                         then Tr.transProp pre true env senv 
                         else (fn (s:Asst.state)=>Asst.True)
      in  emit (A.Directive ("\t.globl "^fid));
          emit (A.Label (fid, NONE));
          if on 
          then emitSpec {lab=fid, asst=(SOME(precond1))}
          else ();
          emit (A.Push A.Ebp);
          emit (A.Movr (A.Esp,A.Ebp));
          emit (A.Push A.Ebx);
          emit (A.Push A.Esi);
          emit (A.Push A.Edi);
          emit (A.Subz (loc,A.Esp));
          emit (A.Jmp funstart);
          emit (A.Label (funstart, NONE));
          if on
          then emitSpec {lab=funstart, asst=(SOME(precond2))}
          else ()
      end
      
(* action: when given frame,emit function of a function, creat epilog for it
 * Note: the size of locals of this function doesn't equal to getLocals only,
 *       but must subtract the size of callee-saved register
 *)
  fun epilog frame post env senv emit emitSpec emitSpec_epi on=
      let val epi = F.getEpilog frame
          val loc = (F.getLocals frame) - (F.getRegSize())
          val postcond = if on
                         then Tr.transProp post true env senv
                         else (fn (s:Asst.state)=>Asst.True)
          val postcond_r = if on
                           then Tr.transProp post false env senv
                           else (fn (s:Asst.state)=>Asst.True)
      in  emit (A.Jmp epi);
          emit (A.Label (epi, NONE));
          if on 
          then emitSpec {lab=epi, asst=(SOME(postcond))}
          else ();
          emit (A.Addz (loc, A.Esp));
          emit (A.Pop A.Edi);
          emit (A.Pop A.Esi);
          emit (A.Pop A.Ebx);
          emit (A.Movr (A.Ebp, A.Esp));
          emit (A.Pop A.Ebp);
          emit (A.Ret);
          if on 
          then (emitSpec_epi {lab="post_condition", asst = (SOME(postcond_r))};(*WIP*)
                emit (A.ExtraAsst(postcond_r)))
          else ()
      end
      
  (*
   *)    
  fun transBinop binop emit emitSpec on = 
      let fun trans (Ast.Plus) = emit (A.Addr(A.Esi, A.Eax))
            | trans (Ast.Minus) = emit (A.Subr(A.Esi, A.Eax))
            | trans (Ast.Times) = emit (A.Mulr(A.Esi, A.Eax))
            | trans (Ast.Divide) = emit (A.Div(A.Esi))
            | trans (Ast.Modus) = (emit (A.Div A.Esi);
                                   emit (A.Movr (A.Edx, A.Eax)))
            | trans (Ast.Equ) = 
              let val truetag = T.newLabel()
                  val endtag = T.newLabel()
              in  emit (A.Beq (A.Esi, A.Eax, truetag));
(*
                  emit (A.Cmpr(A.Esi, A.Eax));
                  emit (A.Je truetag);
*)
                  emit (A.Movz(0, A.Eax));
                  emit (A.Jmp endtag);
                  emit (A.Label (truetag, NONE));
                  if on 
                  then emitSpec {lab=truetag, asst= NONE}
                  else ();
                  emit (A.Movz(1, A.Eax));
                  emit (A.Jmp endtag);
                  emit (A.Label (endtag, NONE));
                  if on 
                  then emitSpec {lab=endtag, asst= NONE}
                  else ()
              end 
            | trans (Ast.NEqu) = 
              let val falsetag = T.newLabel()
                  val endtag = T.newLabel()
              in  emit (A.Beq (A.Esi, A.Eax, falsetag));
(*
                  emit (A.Cmpr(A.Esi, A.Eax));
                  emit (A.Je falsetag);
*)
                  emit (A.Movz(1, A.Eax));
                  emit (A.Jmp endtag);
                  emit (A.Label (falsetag, NONE));
                  if on 
                  then emitSpec {lab=falsetag, asst=NONE}
                  else ();
                  emit (A.Movz(0, A.Eax));
                  emit (A.Jmp endtag);
                  emit (A.Label (endtag, NONE));
                  if on
                  then emitSpec {lab=endtag, asst= NONE}
                  else ()
              end 
            | trans (Ast.GT) = 
              let val truetag = T.newLabel()
                  val endtag = T.newLabel()
              in  emit (A.Bgt (A.Esi, A.Eax, truetag));
(*
                  emit (A.Cmpr(A.Esi, A.Eax));
                  emit (A.Jg truetag);
*)
                  emit (A.Movz(0, A.Eax));
                  emit (A.Jmp endtag);
                  emit (A.Label (truetag, NONE));
                  if on
                  then emitSpec {lab=truetag, asst=NONE}
                  else ();
                  emit (A.Movz(1, A.Eax));
                  emit (A.Jmp endtag);
                  emit (A.Label (endtag, NONE));
                  if on
                  then emitSpec {lab=endtag, asst= NONE}
                  else ()
              end
            | trans (Ast.GE) = 
              let val truetag = T.newLabel()
                  val endtag = T.newLabel()
              in  emit (A.Bge (A.Esi, A.Eax, truetag));
(*
                  emit (A.Cmpr(A.Esi, A.Eax));
                  emit (A.Jge truetag);
*)
                  emit (A.Movz(0, A.Eax));
                  emit (A.Jmp endtag);
                  emit (A.Label (truetag, NONE));
                  if on
                  then emitSpec {lab=truetag, asst= NONE}
                  else ();
                  emit (A.Movz(1, A.Eax));
                  emit (A.Jmp endtag);
                  emit (A.Label (endtag, NONE));
                  if on
                  then emitSpec {lab=endtag, asst= NONE}
                  else ()
              end
            | trans (Ast.LT) = 
              let val falsetag = T.newLabel()
                  val endtag = T.newLabel()
              in  emit (A.Bge (A.Esi, A.Eax, falsetag));
(*
                  emit (A.Cmpr(A.Esi, A.Eax));
                  emit (A.Jge falsetag);
*)
                  emit (A.Movz(1, A.Eax));
                  emit (A.Jmp endtag);
                  emit (A.Label (falsetag, NONE));
                  if on 
                  then emitSpec {lab=falsetag, asst= NONE}
                  else ();
                  emit (A.Movz(0, A.Eax));
                  emit (A.Jmp endtag);
                  emit (A.Label (endtag, NONE));
                  if on
                  then emitSpec {lab=endtag, asst= NONE}
                  else ()
              end
            | trans (Ast.LE) =  
              let val falsetag = T.newLabel()
                  val endtag = T.newLabel()
              in  emit (A.Bgt (A.Esi, A.Eax, falsetag));
(*
                  emit (A.Cmpr(A.Esi, A.Eax));
                  emit (A.Jg falsetag);
*)
                  emit (A.Movz(1, A.Eax));
                  emit (A.Jmp endtag);
                  emit (A.Label (falsetag, NONE));
                  if on 
                  then emitSpec {lab=falsetag, asst=NONE}
                  else ();
                  emit (A.Movz(0, A.Eax));
                  emit (A.Jmp endtag);
                  emit (A.Label (endtag, NONE));
                  if on
                  then emitSpec {lab=endtag, asst=NONE}
                  else ()
              end
            | trans (Ast.Band) = ()
            | trans (Ast.Bor) = ()                                                                                   
      in trans binop
      end
      
  (* action: when given the ast, two env and emit function of left value, 
   *         create the code for computing left value
   * Note: the left value is stored in register eax
   *       the function will return the type of current left value
   *)    
  fun transLval x env senv emit emitSpec on= 
      let fun trans (Ast.Ptr(tp, lval, pos)) =
              let val types = transLval lval env senv emit emitSpec on
                  val newtype = case types
                                 of  E.Pointer(subtype) => subtype
                                   | _=> (Err.impossible "Impossible type! Should be Pointer!"; 
                                          raise Err.Error)
                  val _ = if on 
                          then emit (A.ExtraAsst(fn (st:Asst.state)=>(Asst.Ne(Asst.Sel((#1 st), Asst.Eax), Asst.IntNum(0)))))
                          else ()
                  val _ = emit (A.Movld (0, A.Eax, A.Eax))
              in  newtype
              end
            | trans (Ast.Inarray(lval, exp, s_array, pos)) =
              let val types = transLval lval env senv emit emitSpec on
                  val _ = emit (A.Push A.Eax)
                  val _ = transExp exp env senv emit emitSpec on
                  val _ = emit (A.Pop A.Esi)
                  val newtype = case types
                                 of  E.Array(n, subtype) =>
                                     (if on 
                                      then emit(A.ExtraAsst(
                                                fn st:Asst.state => 
                                                   Asst.And(Asst.Ge(Asst.Sel(#1 st, Asst.Eax), Asst.IntNum(0)),
                                                            Asst.Lt(Asst.Sel(#1 st, Asst.Eax), Asst.IntNum(n)))))
                                      else ();
                                      subtype)
                                   | _ => (Err.impossible "Impossible type! Should be Array!";
                                           raise Err.Error)
                  val elemSize = E.calTypeSize newtype senv
                  val _ = emit (A.Mulz (elemSize, A.Eax))
                  val _ = emit (A.Addr (A.Esi, A.Eax))
              in  newtype
              end
            | trans (Ast.Instruct(lval, id, pos)) = 
              let val types = transLval lval env senv emit emitSpec on
                  val (offset, newtype) = case types
                                           of  E.Struct(s) => Option.valOf (E.lookupF s id senv)
                                            | _ => (Err.impossible "Impossible type! Should be Struct";
                                                    raise Err.Error)
                  val _ = emit (A.Addz (offset, A.Eax))
              in  newtype
              end
            | trans (Ast.Var(id, pos)) =
              let val (islocal, offset, types) = Option.valOf(E.lookup id env)
              in  if islocal
                  then (emit (A.Movr(A.Ebp, A.Eax));
                        emit (A.Addz(offset, A.Eax));
                        types)
                  else (emit (A.Leal(id, A.Eax));
                        types)
              end(* handle Option => (print"*****************************************************************\n"; 
                                    print ("Option.valOf Failed! No such variable "^id^"\n");
                                    print"*****************************************************************\n";
                                    raise Err.Error)
		  *)
	    | trans _ = raise Fail "bug\n"
      in  trans x
      end
  (* action: when given the ast, two env and emit function of the expression, 
   *         create the code for computing the expression
   * Note: the value of expression is stored in register eax
   *       the function will return the type of it
   *)
  and transExp e env senv emit emitSpec on = 
      let fun trans (Ast.Expvoid) = E.Simple
            | trans (Ast.IntNum(i)) = 
              (emit (A.Movz (i, A.Eax));
               E.Simple)
            | trans (Ast.True) =
              (emit (A.Movz (1, A.Eax));
               E.Simple)
            | trans (Ast.False) =
              (emit (A.Movz (0, A.Eax));
               E.Simple)
            | trans (Ast.Null) =
              (emit (A.Movz (0, A.Eax));
               E.Simple)
            | trans (Ast.Lval(lval)) = 
              let val types = transLval lval env senv emit emitSpec on
                  val _ = case types
                           of  E.Simple => emit (A.Movld (0, A.Eax, A.Eax))
                            |  E.Pointer(subtype) => emit (A.Movld (0, A.Eax, A.Eax))
                            | _ => ()
              in  types
              end
            | trans (Ast.BinopExp(e1, Ast.Band, e2, pos)) = 
              let val endtag = T.newLabel()
                  val _ = transExp e1 env senv emit emitSpec on
                  val _ = emit (A.Beqi (0, A.Eax, endtag));
(*
                  val _ = emit (A.Cmpz(0, A.Eax))
                  val _ = emit (A.Je endtag)
*)
                  val _ = transExp e2 env senv emit emitSpec on
                  val _ = emit (A.Jmp endtag)
                  val _ = emit (A.Label (endtag, NONE))
                  val _ = if on 
                          then emitSpec {lab=endtag, asst=NONE}
                          else ()
              in  E.Simple
              end
            | trans (Ast.BinopExp(e1, Ast.Bor, e2, pos)) =
              let val endtag = T.newLabel()
                  val _ = transExp e1 env senv emit emitSpec on
                  val _ = emit (A.Beqi (1, A.Eax, endtag))
(*
                  val _ = emit (A.Cmpz(1, A.Eax))
                  val _ = emit (A.Je endtag)
*)
                  val _ = transExp e2 env senv emit emitSpec on
                  val _ = emit (A.Jmp endtag)
                  val _ = emit (A.Label (endtag, NONE))
                  val _ = if on 
                          then emitSpec {lab=endtag, asst=NONE}
                          else ()
              in  E.Simple
              end
            | trans (Ast.Not(e, pos)) =
              let val endtag = T.newLabel()
                  val falsetag = T.newLabel()
                  val _ = transExp e env senv emit emitSpec on
                  val _ = emit (A.Beqi (0, A.Eax, falsetag))
(*
                  val _ = emit (A.Cmpz(0, A.Eax))
                  val _ = emit (A.Je falsetag)
*)
                  val _ = emit (A.Movz (0, A.Eax))
                  val _ = emit (A.Jmp endtag)
                  val _ = emit (A.Label (falsetag, NONE))
                  val _ = if on 
                          then emitSpec {lab=falsetag, asst=NONE}
                          else ()
                  val _ = emit (A.Movz (1, A.Eax))
                  val _ = emit (A.Jmp endtag)
                  val _ = emit (A.Label (endtag, NONE))
                  val _ = if on 
                          then emitSpec {lab=endtag, asst=NONE}
                          else ()
              in  E.Simple
              end            
            | trans (Ast.BinopExp(e1, binop, e2, pos)) =
              let val _ = transExp e1 env senv emit emitSpec on
                  val _ = emit (A.Push A.Eax)
                  val _ = transExp e2 env senv emit emitSpec on
                  val _ = emit (A.Pop A.Esi)
                  val _ = emit (A.Xchg (A.Esi, A.Eax))
                  val _ = transBinop binop emit emitSpec on
              in  E.Simple
              end
            | trans (Ast.Imply(e1, e2, pos)) = E.Simple (* Cheat Compiler!*)
            | trans (Ast.Forall(id, mytype, exp, pos)) = E.Simple (*Cheat Compiler!*)
            | trans (Ast.Exists(id, mytype, exp, pos)) = E.Simple (*Cheat Compiler!*)
            | trans _ = E.Simple (*Cheat Compiler!*)
      in trans e
      end  

(* aux-function to generate code for array|structure copy *)
  fun bk_copy emit src treg des init stp limit = 
      if init >= limit
      then ()
      else (emit (A.Movld(init, src, treg));
	    emit (A.Movst(treg, init, des));
	    bk_copy emit src treg des (init + stp) stp limit)

(* code generation of sentence
 * action:when given the ast, two env,frame and emit of the sentence, 
 *        create the code of sentence
 * Note: when the assignment sentence assigns value for the whole of struct and array,
 *       it's using the style of memory copy
 *)
  fun transStm stm env senv frame emit emitSpec on =
      let fun trans (Ast.Skip) = ()
            | trans (Ast.AsnExp(lval, exp, pos)) = 
              let val types = transLval lval env senv emit emitSpec on
                  val _ = emit (A.Movr(A.Eax, A.Ebx))
                  val _ = transExp exp env senv emit emitSpec on
              in  case types
                   of  E.Simple => emit (A.Movst(A.Eax, 0, A.Ebx))
                     | E.Pointer(subtype) => emit (A.Movst(A.Eax, 0, A.Ebx))
                     | _ => (*let val size = E.calTypeSize types senv
                                val looptag = T.newLabel()
                            in  emit (A.Movz (size, A.Ecx));
                                emit (A.Movr (A.Eax, A.Esi));
                                emit (A.Jmp looptag);
                                emit (A.Label (looptag, NONE));
                                if on 
                                then emitSpec ({lab=looptag, asst=NONE})
                                else ();
                                emit (A.Movld (0, A.Esi, A.Eax));
                                emit (A.Movst (A.Eax, 0, A.Ebx));
                                emit (A.Subz (4, A.Ecx));
                                emit (A.Addz (4, A.Ebx));
                                emit (A.Addz (4, A.Esi));
                                emit (A.Bgti (0, A.Ecx, looptag))
(*
                                emit (A.Cmpz (0, A.Ecx));
                                emit (A.Jg looptag)
*)
                            end*)
		       let val size = E.calTypeSize types senv
		       in bk_copy emit A.Eax A.Esi A.Ebx 0 4 size
		       end

              end 
            | trans (Ast.AsnAlloc(lval, mytype, pos)) = 
              let val _ = transLval lval env senv emit emitSpec on
                  val size = E.calTypeSize (E.cvtType(mytype)) senv
              in  emit (A.Movr (A.Eax, A.Ebx));
                  emit (A.Movz (size, A.Eax));
                  emit (A.Push A.Eax);
                  emit (A.Call "alloc");
                  emit (A.Addz(4, A.Esp));
                  emit (A.Movst (A.Eax, 0, A.Ebx))
                  (*Init memory, but HOW?*)
              end 
            | trans (Ast.AsnCall(lval, fid, explist, pos)) =
              let val types = transLval lval env senv emit emitSpec on
                  val _ = emit (A.Push A.Eax)
                  val _ = transStm (Ast.Call(fid, explist, pos)) env senv frame emit emitSpec on
              in  case types
                   of  E.Simple => (emit (A.Pop A.Esi);
                                    emit (A.Movst (A.Eax, 0, A.Esi)))
                     | E.Pointer(subtype) =>(emit (A.Pop A.Esi);
                                             emit (A.Movst (A.Eax, 0, A.Esi)))
                     | _ => (*let val size = E.calTypeSize types senv
                                val looptag = T.newLabel()
                            in  emit (A.Movz (size, A.Ecx));
                                emit (A.Movr (A.Eax, A.Esi));
                                emit (A.Pop A.Ebx);
                                emit (A.Jmp looptag);
                                emit (A.Label (looptag, NONE));
                                if on
                                then emitSpec {lab=looptag, asst = NONE}
                                else ();
                                emit (A.Movld (0, A.Esi, A.Eax));
                                emit (A.Movst (A.Eax, 0, A.Ebx));
                                emit (A.Subz (4, A.Ecx));
                                emit (A.Addz (4, A.Ebx));
                                emit (A.Addz (4, A.Esi));
                                emit (A.Bgti (0, A.Ecx, looptag))
(*
                                emit (A.Cmpz (0, A.Ecx));
                                emit (A.Jg looptag)
*)
                            end*)
		       let val size = E.calTypeSize types senv
		       in (emit (A.Pop A.Ebx);
			   bk_copy emit A.Eax A.Esi A.Ebx 0 4 size)
		       end
              end
            | trans (Ast.Return(exp, pos)) = 
              let val epilog = F.getEpilog frame
                  val types = transExp exp env senv emit emitSpec on
                  val _ = case types
                           of  E.Simple =>()
                             | E.Pointer(subtype) =>()
                             | _ => (*(emit (A.Movld (8, A.Ebp, A.Ebx));
                                     let val size = E.calTypeSize types senv
                                         val looptag = T.newLabel()
                                     in  emit (A.Movz (size, A.Ecx));
                                         emit (A.Movr (A.Eax, A.Esi));
                                         emit (A.Jmp looptag);
                                         emit (A.Label (looptag, NONE));
                                         if on
                                         then emitSpec {lab=looptag, asst=NONE}
                                         else ();
                                         emit (A.Movld (0, A.Esi, A.Eax));
                                         emit (A.Movst (A.Eax, 0, A.Ebx));
                                         emit (A.Subz (4, A.Ecx));
                                         emit (A.Addz (4, A.Ebx));
                                         emit (A.Addz (4, A.Esi));
                                         emit (A.Bgti (0, A.Ecx, looptag));
(*
                                         emit (A.Cmpz (0, A.Ecx));
                                         emit (A.Jg looptag);
*)
                                         emit (A.Movld (8, A.Ebp, A.Eax))
                                     end)*)
			       let val size = E.calTypeSize types senv
			       in (emit (A.Movld (8, A.Ebp, A.Ebx));
				   bk_copy emit A.Eax A.Esi A.Ebx 0 4 size;
                                   emit (A.Movld (8, A.Ebp, A.Eax)))
			       end
              in  emit (A.Jmp epilog)
              end
            | trans (Ast.Free (exp, pos)) =
              (transExp exp env senv emit emitSpec on;
               emit (A.Push A.Eax);
               emit (A.Call "free");
               emit (A.Addz(4, A.Esp)))
            | trans (Ast.If(exp, stm1, stm2, pos)) = 
              let val falsetag = T.newLabel()
                  val endtag = T.newLabel()
              in  transExp exp env senv emit emitSpec on;
                  emit (A.Beqi (0, A.Eax, falsetag));
(*
                  emit (A.Cmpz (0, A.Eax));
                  emit (A.Je falsetag);
*)
                  transStm stm1 env senv frame emit emitSpec on;
                  emit (A.Jmp endtag);
                  emit (A.Label (falsetag, NONE));
                  if on 
                  then emitSpec {lab=falsetag, asst= NONE}
                  else ();
                  transStm stm2 env senv frame emit emitSpec on;
                  emit (A.Jmp endtag);
                  emit (A.Label (endtag, NONE));
                  if on
                  then emitSpec {lab=endtag, asst=NONE}
                  else ()
              end
            | trans (Ast.While (inv, exp, s, pos)) = 
              let val looptag = ".L"^(T.gen_name pos)
                  val endtag = T.newLabel()
                  val invs = if on 
                             then Tr.transProp inv true env senv
                             else (fn (s:Asst.state)=>Asst.True)
              in  emit (A.Jmp looptag);
                  emit (A.Label (looptag, NONE));
                  if on
                  then emitSpec {lab=looptag, asst=(SOME(invs))}
                  else ();
                  transExp exp env senv emit emitSpec on;
                  emit (A.Beqi (0, A.Eax, endtag));
(*
                  emit (A.Cmpz(0, A.Eax));
                  emit (A.Je endtag);
*)
                  transStm s env senv frame emit emitSpec on;
                  emit (A.Jmp looptag);
                  emit (A.Label (endtag, NONE));
                  if on
                  then emitSpec {lab=endtag, asst=NONE}
                  else ()
              end
            | trans (Ast.Seq(s1, s2, pos)) = 
              (transStm s1 env senv frame emit emitSpec on;
               transStm s2 env senv frame emit emitSpec on)
            | trans (Ast.Prop(e, pos)) = () (*Cheat Compiler*)
            | trans (Ast.Call (fid, explist, pos)) = 
              let fun pushbkarg emit src treg init stp limit = 
		      if init >= limit
		      then ()
		      else (emit (A.Movld((0-init), src, treg));
			    emit (A.Push treg);
			    pushbkarg emit src treg (init + stp) stp limit)

		  fun pusharg (exp, sum) = 
                      let val types = transExp exp env senv emit emitSpec on
                          val size = E.calTypeSize types senv
                          val _ = case types
                                   of  E.Simple => emit (A.Push A.Eax)
                                     | E.Pointer(subtype) => emit (A.Push A.Eax)
                                     | _ => (*let val looptag = T.newLabel()
                                            in  emit (A.Movz (size, A.Ecx));
                                                emit (A.Addz (size-4, A.Eax));
                                                emit (A.Movr (A.Eax, A.Esi));
                                                emit (A.Jmp looptag);
                                                emit (A.Label (looptag, NONE));
                                                if on
                                                then emitSpec {lab=looptag, asst=NONE}
                                                else ();
                                                emit (A.Movld (0, A.Esi, A.Eax));
                                                emit (A.Push A.Eax);
                                                emit (A.Subz (4, A.Ecx));
                                                emit (A.Subz (4, A.Esi));
                                                emit (A.Bgti (0, A.Ecx, looptag))
(*
                                                emit (A.Cmpz (0, A.Ecx));
                                                emit (A.Jg looptag)
*)
                                            end*)
				       (emit (A.Addz(size-4, A.Eax));
					pushbkarg emit A.Eax A.Esi 0 4 size)
                      in  sum+size
                      end
                  val (_, _, types) = Option.valOf(E.lookup fid env)
              in  case types
                   of  E.Simple => let val argsize = List.foldr pusharg 0 explist
                                   in  emit (A.Call fid);
                                       emit (A.Addz (argsize, A.Esp))
                                   end
                     | E.Pointer(subtype) =>  let val argsize = List.foldr pusharg 0 explist
                                              in  emit (A.Call fid);
                                                  emit (A.Addz (argsize, A.Esp))
                                              end 
                     | _ => let val retsize = E.calTypeSize types senv
                                val _ = emit (A.Subz (retsize, A.Esp))
                                val _ =  emit (A.Leab (0, A.Esp, A.Edi))
                                val argsize = List.foldr pusharg 0 explist
                            in  emit (A.Push A.Edi);
                                emit (A.Call fid);
                                emit (A.Addz (argsize+4+retsize, A.Esp))
                            end
              end handle Option => (print"*****************************************************************\n"; 
                                    print ("Option.valOf Failed! No such variable "^fid^"\n");
                                    print"*****************************************************************\n";
                                    raise Err.Error)
      in  trans stm
      end
      
(* the code generation of function
 * action: when given ast and two environments, generate code of function
 * the new generated code is filled into proclist as a list
 *)
  fun transFun (fid, rettype, arg, var, stm, pre, post) env senv proclist speclist specindexlist speccoqlist prooflist has_proof = 
      let val frame = F.newFrame fid rettype
          (* build variable env in function *)
          val env1 = B.buildEnv arg env senv frame F.allocArgs
          val newenv = B.buildEnv var env1 senv frame F.allocLocals
          val code = ref []  (* assembly code list *)
          val specs = ref []  (* real specification list *)
          val nospecindex = ref []  (* label list that no real specification in it *)
          val specindex = ref []  (* label list that has real specification in it *)
          (* insert real specification to the specification list and 
           * mark the label to has-specification or no-specification by inserting them to the corresponding index list *)
          fun emitSpec (spec:Asst.spec) = 
              (specs := spec ::(!specs);
               case (#asst spec)
                of  NONE => nospecindex := (#lab spec) :: (!nospecindex)
                  | _ => specindex := (#lab spec) :: (!specindex))
          (* in the epilog, there must be real specification in the end label*)
          fun emitSpec_epi (spec:Asst.spec) =
              specs := spec ::(!specs)
(* 
               if (#asst spec) = NONE
               then specindex := (#lab spec) :: (!specindex)
               else specindex := (!specindex)@[#lab spec]) 
*)
          fun emit instr = code:= instr ::(!code)
          (* generate assembly code and emit translated specification *)
          val _ = transStm stm newenv senv frame emit emitSpec has_proof
          val body' = !code
          val _ = code:=[]
          (* generate prolog code and specification *)
          val _ = prolog frame pre newenv senv emit emitSpec has_proof
          val prolog = !code
          (* generate epilog and specification *)
          val _ = code:=[]
          val _ = epilog frame post newenv senv emit emitSpec emitSpec_epi has_proof
          (* get rid of redundent jmp instruction *)
          fun filt_jmp code =
              let fun filt [] = []
                    | filt ((A.Jmp(l))::code') = 
                      (case code'
                        of  (A.Jmp(l'))::code'' => filt code'
                          |  _ => ((A.Jmp(l))::(filt code')))
                    | filt (i :: code') = i :: (filt code')
              in  filt code
              end
          (* "whole" is the code list that in positive sequence, that is, the first instruction is in the head of the list*)
	  val body = OptonASM.reorg_asm(filt_jmp (body'))
          val whole = List.rev (filt_jmp ((!code)@body@prolog))

          val proof1 = if has_proof 
                       then PG.prf_list_gen_1 (!nospecindex) whole specs
                       else []
          val proof2 = if has_proof
                       then (PG.prf_list_gen_2 (!specindex) whole specs) @ proof1
                       else []
          val (newspecs, spec_coqtext) = LCoq.pr_specs (!specs)
          val spec_name = "CodeHeapType_"^fid
          val cdhptp = LCoq.pr_heapspec spec_name newspecs
          val spec_coqtext = spec_coqtext @ [cdhptp]
	  val _ = PG.Current_Hty := spec_name
          val real_p_l = List.map (PG.gen_wf_lemma env senv (spec_name, newspecs, (!specs))) proof2
          fun filt_spec specs = 
              let fun get_hd s = String.substring(s, 0, 3)
                  fun filt [] = []
                    | filt ({lab=l, asst = a}::speclist) = 
                      if String.size(l)<=3
                      then {lab=l, asst=a} :: (filt_spec speclist)
                      else let val head = get_hd l
                           in  if head = "..A" 
                               then filt_spec speclist
                               else {lab=l, asst=a} :: (filt_spec speclist)
                           end
              in  filt specs
              end
          val filted_specs = filt_spec (!specs)
          val _ = proclist := whole::(!proclist)
          val _ = if has_proof 
                  then ((speclist := filted_specs :: (!speclist));
                        (specindexlist := newspecs ::(!specindexlist));
                        (speccoqlist := spec_coqtext :: (!speccoqlist));
                        (prooflist := real_p_l :: (!prooflist)))
                  else ()
      in  ()
      end
      
(* the code generation of data segment
 * action: when given the offest table of the globals env and the senv
 *         generate code for the globals of the programe
 *)
  fun transData env senv =
      let val code = ref []
          fun emit instr = code := instr:: (!code)
          fun filt (id, (islocal, offset, types)) = 
              let val size = Int.div(((E.calTypeSize types senv) + 1), 4)
              in  (id, size)
              end
          fun select (id, (islocal, offset, types)) =
              if offset = ~1 
              then true
              else false
          fun gendata (id, size) = 
              if size = 1
              then (emit (A.Label (id, NONE));
                    emit (A.Directive ("\t.long 0")))
              else (emit (A.Label (id, NONE));
                    emit (A.Directive ("\t.rept "^ Int.toString(size)));
                    emit (A.Directive ("\t.long 0"));
                    emit (A.Directive ("\t.endr")))
      in  List.app gendata (List.map filt (List.filter select env));
          List.rev (!code)
      end

(* the code generation of programe
 * action: when given ast of programe, generate code for programe
 *)
   fun transProg ast has_proof = 
       let val proclist = ref[]  (*function codes' list*)
           val speclist = ref[]  (* real specifications' list *)
           val specindexlist = ref[] (* specification and index's list *)
           val speccoqlist = ref []  (* specifications list which is in coq style*)
           val prooflist = ref[]  (* code block proof *)
           val env = ref (E.create()) (* variable invariants *)
           val senv = ref (E.creat()) (* structure type environment *)
           (* build environments *)
           fun build (Ast.ExdecSkip) = ()
             | build (Ast.ExdecStruct(id, fieldlist, pos)) = 
               senv := B.buildSEnv id fieldlist (!senv)
             | build (Ast.ExdecVar(varlist, pos)) = 
               env := B.buildGEnv varlist (!env)
             | build (Ast.ExdecFunc(id, rettype, arg, var, stm, pre, post, pos)) =
               env := B.buildFEnv (id, rettype) (!env)    
             | build (Ast.ExdecSeq(s1, s2, pos)) = (build s1; build s2)
           (* generate assembly code and proofs *)
           fun trans (Ast.ExdecFunc(id, rettype, arg, var, stm, pre, post, pos)) = 
               transFun (id, rettype, arg, var, stm, pre, post) (!env) (!senv) 
                        proclist speclist specindexlist speccoqlist prooflist has_proof
             | trans (Ast.ExdecSeq(s1, s2, pos)) = (trans s1; trans s2)
             | trans _ = ()
           val _ = build ast
           val _ = trans ast
           val allspec = List.concat(!speclist)
           val allspecindex = List.concat (!specindexlist)
           val allspeccoq = List.concat (!speccoqlist)
           val allproof = List.concat(!prooflist)
           val text = (A.Section(A.Text))::
                      (A.Directive("\t.align 4"))::
                      List.concat(List.rev (!proclist))
           val data = (A.Section(A.Data))::
                      (A.Directive("\t.align 4"))::
                      (transData (!env) (!senv))
       in  (text, data, allspec, allspecindex, allspeccoq, allproof)
       end

(*action: transform the input ast into code string and output the result into .s file
 *)
  fun emitCode ast has_proof=
      let val cpright = "# Copyright (C) by LSS team. All rights reserved.\n\n"
          val assemblyfile = TextIO.openOut((!Err.fileName)^".s")
          val coqfile = TextIO.openOut((!Err.fileName)^".v")
          (* (code, data code, real specification, specification name and its corresponding index, 
           *  specification in coq, code block proof) *)
          val (text, data, spec, specindex, speccoq, proof) = transProg ast has_proof
          (* (code segment) generate assembly code, assertions will be output in annotations. *)
          val code =String.concat((List.map (Ts.toString (not has_proof) spec) text))
          (* data segment *)
          val dataseg =String.concat((List.map(Ts.toString true spec) data))
          (* assembly code that can run in the machine*)
          val whole = (cpright ^ code ^ dataseg)
          (* specifications in coq *)
          val spec_coqtext = String.concat speccoq
          fun nullemit str:string = str
          (* output code block well-formed lemma and its proof *)
          fun p2coq (lab, lem, prf) = 
              let val lab' = String.map LCoq.filt lab
                  val lemma = "\nLemma "^lab'^"_infer: "^(LCoq.pr_pterm 2 ~1 3 nullemit specindex lem)^".\n"
                  val proof = String.concat (List.map (LCoq.pr_tactic specindex) prf)
              in lemma^proof^"\n"
              end
          (* all the code blocks' well-formed lemma and corresponding proof *)
          val proof_coqtext' = List.map p2coq proof
          val proof_coqtext = String.concat proof_coqtext'
      in  TextIO.output(assemblyfile, whole);
          TextIO.closeOut(assemblyfile);
          (if has_proof
           then (TextIO.output(coqfile, spec_coqtext ^ proof_coqtext);
                 TextIO.closeOut(coqfile))
           else ());
          specindex
      end
end


